0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 88 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 22 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
app3_aC_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appA_in_gga(T18, T11, T13))
appA_in_gga([], T25, T25) → appA_out_gga([], T25, T25)
appA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appA_out_gga(T35, T36, T38)) → appA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appA_out_gga(T18, T11, T13)) → app3_aC_out_ggga([], T18, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, X50))
appB_in_gga([], T59, T59) → appB_out_gga([], T59, T59)
appB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appB_out_gga(T67, T68, X74)) → appB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, X50)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appA_out_gga(.(T47, T52), T11, T13)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
app3_aC_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appA_in_gga(T18, T11, T13))
appA_in_gga([], T25, T25) → appA_out_gga([], T25, T25)
appA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appA_out_gga(T35, T36, T38)) → appA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appA_out_gga(T18, T11, T13)) → app3_aC_out_ggga([], T18, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, X50))
appB_in_gga([], T59, T59) → appB_out_gga([], T59, T59)
appB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appB_out_gga(T67, T68, X74)) → appB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, X50)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appA_out_gga(.(T47, T52), T11, T13)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
APP3_AC_IN_GGGA([], T18, T11, T13) → U3_GGGA(T18, T11, T13, appA_in_gga(T18, T11, T13))
APP3_AC_IN_GGGA([], T18, T11, T13) → APPA_IN_GGA(T18, T11, T13)
APPA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → U1_GGA(T34, T35, T36, T38, appA_in_gga(T35, T36, T38))
APPA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPA_IN_GGA(T35, T36, T38)
APP3_AC_IN_GGGA(.(T47, T48), T49, T11, T13) → U4_GGGA(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, X50))
APP3_AC_IN_GGGA(.(T47, T48), T49, T11, T13) → APPB_IN_GGA(T48, T49, X50)
APPB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → U2_GGA(T66, T67, T68, X74, appB_in_gga(T67, T68, X74))
APPB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPB_IN_GGA(T67, T68, X74)
APP3_AC_IN_GGGA(.(T47, T48), T49, T11, T13) → U5_GGGA(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, T52))
U5_GGGA(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → U6_GGGA(T47, T48, T49, T11, T13, appA_in_gga(.(T47, T52), T11, T13))
U5_GGGA(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → APPA_IN_GGA(.(T47, T52), T11, T13)
app3_aC_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appA_in_gga(T18, T11, T13))
appA_in_gga([], T25, T25) → appA_out_gga([], T25, T25)
appA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appA_out_gga(T35, T36, T38)) → appA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appA_out_gga(T18, T11, T13)) → app3_aC_out_ggga([], T18, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, X50))
appB_in_gga([], T59, T59) → appB_out_gga([], T59, T59)
appB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appB_out_gga(T67, T68, X74)) → appB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, X50)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appA_out_gga(.(T47, T52), T11, T13)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
APP3_AC_IN_GGGA([], T18, T11, T13) → U3_GGGA(T18, T11, T13, appA_in_gga(T18, T11, T13))
APP3_AC_IN_GGGA([], T18, T11, T13) → APPA_IN_GGA(T18, T11, T13)
APPA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → U1_GGA(T34, T35, T36, T38, appA_in_gga(T35, T36, T38))
APPA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPA_IN_GGA(T35, T36, T38)
APP3_AC_IN_GGGA(.(T47, T48), T49, T11, T13) → U4_GGGA(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, X50))
APP3_AC_IN_GGGA(.(T47, T48), T49, T11, T13) → APPB_IN_GGA(T48, T49, X50)
APPB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → U2_GGA(T66, T67, T68, X74, appB_in_gga(T67, T68, X74))
APPB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPB_IN_GGA(T67, T68, X74)
APP3_AC_IN_GGGA(.(T47, T48), T49, T11, T13) → U5_GGGA(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, T52))
U5_GGGA(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → U6_GGGA(T47, T48, T49, T11, T13, appA_in_gga(.(T47, T52), T11, T13))
U5_GGGA(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → APPA_IN_GGA(.(T47, T52), T11, T13)
app3_aC_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appA_in_gga(T18, T11, T13))
appA_in_gga([], T25, T25) → appA_out_gga([], T25, T25)
appA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appA_out_gga(T35, T36, T38)) → appA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appA_out_gga(T18, T11, T13)) → app3_aC_out_ggga([], T18, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, X50))
appB_in_gga([], T59, T59) → appB_out_gga([], T59, T59)
appB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appB_out_gga(T67, T68, X74)) → appB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, X50)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appA_out_gga(.(T47, T52), T11, T13)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
APPB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPB_IN_GGA(T67, T68, X74)
app3_aC_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appA_in_gga(T18, T11, T13))
appA_in_gga([], T25, T25) → appA_out_gga([], T25, T25)
appA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appA_out_gga(T35, T36, T38)) → appA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appA_out_gga(T18, T11, T13)) → app3_aC_out_ggga([], T18, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, X50))
appB_in_gga([], T59, T59) → appB_out_gga([], T59, T59)
appB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appB_out_gga(T67, T68, X74)) → appB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, X50)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appA_out_gga(.(T47, T52), T11, T13)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
APPB_IN_GGA(.(T66, T67), T68, .(T66, X74)) → APPB_IN_GGA(T67, T68, X74)
APPB_IN_GGA(.(T66, T67), T68) → APPB_IN_GGA(T67, T68)
From the DPs we obtained the following set of size-change graphs:
APPA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPA_IN_GGA(T35, T36, T38)
app3_aC_in_ggga([], T18, T11, T13) → U3_ggga(T18, T11, T13, appA_in_gga(T18, T11, T13))
appA_in_gga([], T25, T25) → appA_out_gga([], T25, T25)
appA_in_gga(.(T34, T35), T36, .(T34, T38)) → U1_gga(T34, T35, T36, T38, appA_in_gga(T35, T36, T38))
U1_gga(T34, T35, T36, T38, appA_out_gga(T35, T36, T38)) → appA_out_gga(.(T34, T35), T36, .(T34, T38))
U3_ggga(T18, T11, T13, appA_out_gga(T18, T11, T13)) → app3_aC_out_ggga([], T18, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U4_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, X50))
appB_in_gga([], T59, T59) → appB_out_gga([], T59, T59)
appB_in_gga(.(T66, T67), T68, .(T66, X74)) → U2_gga(T66, T67, T68, X74, appB_in_gga(T67, T68, X74))
U2_gga(T66, T67, T68, X74, appB_out_gga(T67, T68, X74)) → appB_out_gga(.(T66, T67), T68, .(T66, X74))
U4_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, X50)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
app3_aC_in_ggga(.(T47, T48), T49, T11, T13) → U5_ggga(T47, T48, T49, T11, T13, appB_in_gga(T48, T49, T52))
U5_ggga(T47, T48, T49, T11, T13, appB_out_gga(T48, T49, T52)) → U6_ggga(T47, T48, T49, T11, T13, appA_in_gga(.(T47, T52), T11, T13))
U6_ggga(T47, T48, T49, T11, T13, appA_out_gga(.(T47, T52), T11, T13)) → app3_aC_out_ggga(.(T47, T48), T49, T11, T13)
APPA_IN_GGA(.(T34, T35), T36, .(T34, T38)) → APPA_IN_GGA(T35, T36, T38)
APPA_IN_GGA(.(T34, T35), T36) → APPA_IN_GGA(T35, T36)
From the DPs we obtained the following set of size-change graphs: